Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
01(0(*(*(x1)))) → 11(1(x1))
11(1(*(*(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(0(#(#(x1))))
#1(#(1(1(x1)))) → #1(x1)
11(1(*(*(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(1(#(#(x1))))
11(1(*(*(x1)))) → 01(0(#(#(x1))))
11(1(*(*(x1)))) → #1(x1)
#1(#(1(1(x1)))) → #1(#(x1))
#1(#(0(0(x1)))) → #1(x1)
#1(#(0(0(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(#(#(x1)))
01(0(*(*(x1)))) → 11(x1)
The TRS R consists of the following rules:
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
01(0(*(*(x1)))) → 11(1(x1))
11(1(*(*(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(0(#(#(x1))))
#1(#(1(1(x1)))) → #1(x1)
11(1(*(*(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(1(#(#(x1))))
11(1(*(*(x1)))) → 01(0(#(#(x1))))
11(1(*(*(x1)))) → #1(x1)
#1(#(1(1(x1)))) → #1(#(x1))
#1(#(0(0(x1)))) → #1(x1)
#1(#(0(0(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(#(#(x1)))
01(0(*(*(x1)))) → 11(x1)
The TRS R consists of the following rules:
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.